Section: New Results

Synchronous symbolic translation systems for translation validation

Participants : Van-Chan Ngo, Jean-Pierre Talpin.

We propose a framework for verification of the correct implementation of the SIGNAL compiler's generation code task. In order to present the formal semantics of SIGNAL and generated code programs we introduce synchronous symbolic transition system (SSTS) which is the computational model of our formal verification approach. We denote ${𝒟}_{𝒱}=\prod _{i\in [1,n]}{𝒟}_{v_i}$ as the domain of a set of variables $𝒱=(v_1,...,v_n)$. A set of states $P\subset {𝒟}_{𝒱}$ is defined as a predicate over the set of variables $𝒱$ such that the predicate is held in $P$. An assignment $A$ is a function $A:{𝒟}_{𝒱}\mapsto {𝒟}_{𝒱}$ that the values of the variable set $𝒱$. A SSTS is a tuple $L=(𝒱,\Theta ,\Gamma ,ℰ)$ where:

• $𝒱=(v_1,...,v_n)$ is a set of variables,

• $\Theta \subseteq {𝒟}_{𝒱}$ is a predicate on $𝒱$ defining the initial condition on the variable set,

• $\Gamma$ is a finite set of symbolic transitions $\gamma =(P_{\gamma },A_{\gamma })$ where:

  • $P_{\gamma }\subseteq {𝒟}_{𝒱}$ is a predicate on $𝒱$, which guards $\gamma$

  • $A_{\gamma }:{𝒟}_{𝒱}\to {𝒟}_{𝒱}$ is the assignment function of $\gamma$

• $ℰ\subseteq 𝒱$ is a set of externally observable variables.

The generated code correctly implements the SIGNAL program if and only if there is a refinement for their SSTSs and we say that the generated code's SSTS refines the SIGNAL program's SSTS. This framework also works with SIGNAL programs which is considered as infinite state systems. To obtain the verification results, we apply abstraction interpretation techniques [39] which provide over-approximations of the refinement relation between the input SIGNAL program's model and the output generated code's model.